Require Import ZArith.
  Open Scope Z_scope.

  Inductive even: Z -> Prop :=
    | even_base: even 0
    | even_succ: forall n, odd (n - 1) -> even n

  with odd: Z -> Prop :=
    | odd_succ: forall n, even (n - 1) -> odd n.

 Functional Scheme even_odd_mutual_ind := Induction for even Sort Prop.